$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$ List), $e$:E, $a$:$A$.
\\[0ex]($a$ $\in$ es{-}interface{-}history(${\it es}$;$X$;$e$)) $\Leftarrow\!\Rightarrow$ ($\exists$${\it e'}$:E. (($\uparrow$(${\it e'}$ $\in_{b}$ $X$)) \& ${\it e'}$ $\leq$loc $e$  \& ($a$ $\in$ $X$(${\it e'}$))))